Exact Inverse Relations: Eq 146, 150, 156 through Eq 160

This Pull Request adds proofs for equations 156 through 160. In addition equations 156 and 158 have "Hermitianized" versions, where the Hermitian operator is used instead of the transpose. These might be more appropriate (or what the reader understands when thinking of comlelx matrices).

The file mat_inv_lib.lean contains support identities. These are:

1. is_unit_of_pos_def: a positive definite matrix is also a unit determinant matrix (basically fancy way of saying determinant is nonzero).
2. invertible_of_pos_def: a positive definite matrix is invertible.
3. A_add_B_P_Bt_pos_if_A_pos_B_pos: Given $P,R$ positive definite the sum of $ R + BPB^H$ is positive definite.
4. right_mul_inj_of_invertible: multiplication from the right by invertible matrices is injective.
5. left_mul_inj_of_invertible: multiplication from the the left by invertible matrices is injective.
6. unit_matrix_sandwich: a matrix unit unit R i.e. a matrix with one element interposed in an outerproduct can be removed to the left to be scalar multiplication by that one element.
   $$u,v \in \mathbb{C}^{m\times 1}, s \in \mathbb{C}^{1 \times 1} \to [s]_{1,1} (uv^t) = u \cdot s \cdot v^t$$

With $\cdot{}$, meaning matrix multiplication and $[A]_{ab}$ meaning element a,b from matrix $A$:

7. row_mul_mat_mul_col: a weighted inner product of row and vector columns with a weight matrix in the middle can be regraded as scalar or one element matrix.
   $$u^T A v = u^T \cdot A \cdot v$$
8. one_add_row_mul_mat_col_inv
   $$(1 + c^T A b)^{-1} = [(1 + u^T \cdot A \cdot v)^{-1}]_{1,1}$$